%There are two aspects that make the used verification approach
%applicable in practice.
We claim that the verification approach is practical to use for two reasons.
First, the used approach provides a fully automated translation
from ATL transformations and their constrained metamodels to OCL and relational
logic. The approach further provides a fully automated verification of the
generated translation. 
% We also demonstrated how such an automated verification
% approach to a real, industrial transformation problem. 
Even when applied to a realistic case study, the approach scaled to a scope that
was large enough to strongly suggest that the analysis did not overlook a bug in
the transformation due to the boundedness of the underlying satisfiability
solving approach. If we wanted to perform the same verification on a Java
implementation of the transformation, we would require equally rich class and
operation contracts for, say, Ecore in JML~\cite{Jacobs01}. To the best of our
knowledge, no research has explored automatically inferring such contracts. Even
then, we expect that the user would have to explicitly specify loop invariants
as soon as the transformation contains non-trivial loops, like the loops
in our transformation.

Second, the study translates a substantial subset of ATL for
verification, i.e., all rules except for imperative blocks, recursive lazy
rules and recursive query operations other than relational closures. Thus, the
approach takes advantage of the ways declarative, rule-based transformation
languages (e.g., ATL) provide to iterate over the input model without requiring
recursion or looping.
This simplifies verification by, for instance, obviating the need
for loop invariants. Although this subset of ATL is not Turing-complete, it can
be used to implement many non-trivial transformations.  We have statically
checked the 131 transformations (comprising 2825 individual rules) in the ATL
transformation zoo~\cite{ZOO}, and 83 of them fall into the described fragment,
i.e., neither use recursive rules nor imperative features. Of the remaining 48
transformations, 24 of them that use imperative blocks but no
recursion could be expressed declaratively, too.

% These two points strongly motivate the use of specific transformation languages 
% and verification approaches similar to our approach instead of using general
% purpose imperative programming languages for which no such automated
% verification has been developed.
We conclude that our verification approach greatly benefited from the
conceptual simplicity of the declarative fragment of ATL compared to, e.g., a
general-purpose programming language such as Java.